Problem:
 f(a,empty()) -> g(a,empty())
 f(a,cons(x,k)) -> f(cons(x,a),k)
 g(empty(),d) -> d
 g(cons(x,k),d) -> g(k,cons(x,d))

Proof:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    g1(10,5) -> 3*
    g1(1,10) -> 4*
    g1(7,5) -> 3*
    g1(2,5) -> 3*
    g1(2,7) -> 4*
    g1(1,5) -> 3*
    g1(1,7) -> 4*
    g1(2,10) -> 4*
    cons1(2,12) -> 5*
    cons1(2,14) -> 5*
    cons1(1,2) -> 7*
    cons1(1,10) -> 7*
    cons1(1,12) -> 5*
    cons1(1,14) -> 5*
    cons1(2,1) -> 7*
    cons1(2,5) -> 5*
    cons1(2,7) -> 7*
    cons1(1,1) -> 7*
    cons1(1,5) -> 5*
    cons1(1,7) -> 7*
    cons1(2,2) -> 10*
    cons1(2,10) -> 7*
    f1(10,1) -> 3*
    f1(7,1) -> 3*
    f1(10,2) -> 3*
    f1(7,2) -> 3*
    empty1() -> 5*
    g2(7,12) -> 3*
    g2(2,12) -> 3*
    g2(7,14) -> 3*
    g2(2,14) -> 3*
    g2(1,12) -> 3*
    g2(1,14) -> 3*
    g2(10,12) -> 3*
    g2(10,14) -> 3*
    f0(1,2) -> 3*
    f0(2,1) -> 3*
    f0(1,1) -> 3*
    f0(2,2) -> 3*
    cons2(2,12) -> 12*
    cons2(2,14) -> 12*
    cons2(1,12) -> 12*
    cons2(1,14) -> 12*
    cons2(2,5) -> 14*
    cons2(1,5) -> 12*
    empty0() -> 1*
    g0(1,2) -> 4*
    g0(2,1) -> 4*
    g0(1,1) -> 4*
    g0(2,2) -> 4*
    cons0(1,2) -> 2*
    cons0(2,1) -> 2*
    cons0(1,1) -> 2*
    cons0(2,2) -> 2*
    1 -> 4*
    2 -> 4*
    5 -> 3*
    7 -> 4*
    10 -> 4*
    12 -> 3*
    14 -> 3*
  problem:
   
  Qed